Nuprl Lemma : ma-shape_wf
0,22
postcript
pdf
M
:msga{i:l}. ma-shape{i:l}(
M
)
Type{i'}
latex
Definitions
MsgA
,
t
T
,
x
:
A
.
B
(
x
)
,
da(
M
)
,
ds(
M
)
,
MsgA(
ds
;
da
)
,
Shape(
M
)
Lemmas
msga-body
wf
,
ma
ds
wf
,
ma
da
wf
,
msga
wf
origin
M:msga{i:l}. ma-shape{i:l}(M) 
Type{i'} M:msga{i:l}. ma-shape{i:l}(M) Type{i'} Tx:A. B(x)